Dynamic checkers are used to check for the presence of various kinds of errors in software programs, such as assertion failures or violations, memory errors, and divide-by-zero errors to name a few. Examples of popular tools with dynamic checker functionality include some memory analyzers, profilers, and coverage analyzers.
In a typical implementation, a dynamic checker analyzes a software program by executing the software program using a test suite including one or more concrete inputs. The concrete inputs are identified and provided manually by a user. To detect errors, a user has to provide concrete inputs that trigger the errors. Accordingly, it is difficult to maintain a high-quality test suite which exercises sufficiently many paths in the software program and which catches corner-case bugs.
Symbolic execution is a technique for dynamically analyzing a software program. Symbolic execution uses as input values symbolic values instead of actual data and represents values of program variables as symbolic expressions. As a result, the outputs computed by a software program that is symbolically executed are expressed as a function of the symbolic inputs. Through symbolic execution, each path within a software program may be symbolically executed.
Some dynamic checkers implement symbolic execution, and may be referred to as symbolic execution based dynamic checkers. Conventional symbolic execution based dynamic checkers have limited defect detection, such as detection of simple memory errors including null pointer errors and out-of-bound access errors. Moreover, the detectable types of defects in conventional symbolic execution based dynamic checkers are hardcoded such that users are unable to easily change the types of defects that are detected.
The subject matter claimed herein is not limited to embodiments that solve any disadvantages or that operate only in environments such as those described above. Rather, this background is only provided to illustrate one example technology area where some embodiments described herein may be practiced.